#!/usr/bin/python

import re
import os
import sys
debug = True

lines = sys.stdin.readlines()
lemma = sys.argv[1]

# INPUT:
# - lines contain a list of "%i:goal" where "%i" is the index of the goal
# - lemma contain the name of the lemma under scrutiny
# OUTPUT:
# - (on stdout) a list of ordered index separated by EOL


rank = []             # list of list of goals, main list is ordered by priority
maxPrio = 50
for i in range(0,maxPrio):
  rank.append([])


if lemma == "helpingUpdateKey":
  # only prioritize ReaderK() and TagK() goals and then full auto mode
  for line in lines:
    num = line.split(':')[0]
    if debug: sys.stderr.write(line)
      
    if re.match('.*ReaderK\(.*', line):
      rank[30].append(num)
    elif re.match('.*TagK\(.*', line):
      rank[20].append(num)
    else:
      rank[5].append(num)

elif lemma == "helpingOutNotKey":
  # !Tag and !Reader facts
  for line in lines:
    num = line.split(':')[0]
    if debug: sys.stderr.write(line)

    if (re.match('.*!Tag\(.*', line) or
        re.match('.*!Reader\(.*', line) or
        re.match('.*ReaderState1\(.*', line)):
      rank[9].append(num)
    elif re.match('.*TagK\(.*', line):
      rank[4].append(num)
    else:
      rank[5].append(num)


elif lemma == "helpingSecrecy" or lemma == "noninjectiveagreementTAG":
  # Difficulty here: one has to find the appropriate splitEqu() goal.
  # Choosing the wrong one results in a very large number of uncessary subgoals.
  # The criterion: the one that instantiates the inputs of the rule R whose the output
  # is coerced into the term t that is considered known by the attacker (starting with K(t)).
  # Criterion is easily applicable in practice but impossible to implement in an oracle (no access to the equation).

  # TODO implement:
  # 1. Impossible to have Key or Update of some term of the form h(term) when term is not some hash
     # solve( Update( h((~r0.1 xor h(k0) xor h((~r0.1XORr1.1XORh(k0))))), 'R1') @ #j.1 )
     # --> solve( Update( h((~r0.1XORh(k0)XORh((~r0.1XORr1.1XORh(k0))))),'R2' @ #j.7 )
  # 2. When nothing is known about k0 and K(k0), use appropriate Update(k0) twice --> inductive hypothesis
  # 3. Too many different cases of K(t) to treat. Have a criterion like t= h() XOR t' or t=h(t' XOR h())
  # 4. For nonInjectiveagreementTAG: add Running() as a top-priority goal. Also add !KD( (x.1 XOR x.2) .

  # NEW BUILD: almost get autoproof for secrecy, ideas:
  # a lot of cases are resolved by focusing on goals like 9. solve( Update( h((~r0 XOR h(k0) XOR h(h(k0)))), 'R2'
  # because we have a reuse lemma stating that if one has Update(t) then t = h(t') so going through Update() twice gives a contradiction
  # solve( Update( h((~r0 XOR h(k0) XOR h((~r0 XOR r1 XOR h(k0))))), 'R2'
  # - Give weight to goals. For example if goal is KU(t) with t small but containing fresh values -> big priority
  for line in lines:
    num = line.split(':')[0]
    if debug: sys.stderr.write(line)

    if lemma == "noninjectiveagreementTAG":
      if (re.match('.*Running\(.*', line) or
          re.match('.*splitEqs\(7.*', line)):
        rank[47].append(num)
      elif (re.match('.*!K.\(.*x\.1.*', line)):
        rank[46].append(num)

    if re.match('.*~~>.*', line):
      rank[48].append(num)
    if (re.match('.*!KU\( ~k.*', line)):
      rank[46].append(num)
    elif (re.match('.*!KU\( h\(~k.*', line)):
      rank[44].append(num)
    elif (re.match('.*!KU\( h\(k0\).*', line) or
          re.match('.*!KU\( h\(h\(k0', line)):
      rank[42].append(num)
    elif (re.match('.*!K.\(.*r1\.1.*', line) or
          re.match('.*!K.\(.*r1.*', line) or
          re.match('.*!K.\(\(.*z1\.1.*', line) or
          re.match('.*!K.\(\(.*z1.*', line) or
          re.match('.*!K.\(\(.*~r0\.1.*', line) or
          re.match('.*!K.\(\(.*~r0.*', line) or
          re.match('.*!K.\( \(.*~r0\.1.*', line) or
          re.match('.*!K.\( \(.*~r0.*', line) or
          re.match('.*!K.\( ~r.*', line) or
          re.match('.*!K.\( \(z.1', line) or
          re.match('.*!K.\( \(h\(k0.*h\(.*', line) or
          re.match('.*!K.\(.*x.*h.*', line)):          
      rank[40].append(num)
    elif (re.match('.*!KU\(.*r1\.1.*', line) or
          re.match('.*!KU\(.*r1.*', line)):
      rank[35].append(num)
    elif (re.match('.*!Tag\(.*', line) or
          re.match('.*!Reader\(.*', line) or
          re.match('.*ReaderState1\(.*', line) or
          re.match('.*TagState1\(.*', line)):
      rank[30].append(num)
    elif (re.match('.*ReaderState1\(.*', line) or
          re.match('.*TagState1\(.*', line)):
      rank[27].append(num)
    elif (re.match('.*!K.\( \(x.*h\(k0', line)):
      rank[22].append(num)
    elif (re.match('.*splitEqs\(2\.*', line)):
      rank[17].append(num)
    elif (re.match('.*splitEqs\(3\.*', line)):
      rank[15].append(num)
    elif (re.match('.*!KU\( ~k.*', line)):
      rank[46].append(num)
    else:
      rank[5].append(num)


elif lemma == "noninjectiveagreementREADER":
  for line in lines:
    num = line.split(':')[0]
    if debug: sys.stderr.write(line)
      
    if re.match('.*Update\(.*', line):
      rank[0].append(num)
    else:
      rank[5].append(num)
  
elif lemma == "executable":
  # only prioritize ReaderK() and TagK() goals and then full auto mode
  for line in lines:
    num = line.split(':')[0]
    if debug: sys.stderr.write(line)
      
    if re.match('.*Update\(.*', line):
      rank[0].append(num)
    else:
      rank[5].append(num)


# elif lemma == "injectiveagreement_UE_HSS_KASME" or \
#      lemma == "injectiveagreement_HSS_UE_KASME":

#   for line in lines:
#     num = line.split(':')[0]
#     if debug:
#       sys.stderr.write(line)

#     # Before default
#     if   re.match('.*!KU\( ~K.*', line): rank[92].append(num)
#     elif re.match('.*!KU\( \(f5_star\(.*', line) or \
# 	 re.match('.*!KD\( \(f5_star\(.*', line): rank[86].append(num)
#     elif re.match('.*!KU\( f1_star\(~K.*', line): rank[85].append(num)
#     elif re.match('.*ARPFEntry\(.+\(~sqn\+~sqn\).*', line): rank[75].append(num)
#     elif re.match('.*!Ltk_Sym\(.*', line): rank[70].append(num)

#     elif re.match('.*!KU\( f1\(~K,.*', line): rank[50].append(num)
#     elif re.match('.*RcvS\(.*', line): rank[45].append(num)
#     elif re.match('.*!KU\( \(f5\(~K,.*', line) or \
# 	 re.match('.*!KD\( \(f5\(~K,.*', line): rank[40].append(num)
#     elif re.match('.*St_3_SEAF\(.*', line): rank[30].append(num)
#     elif re.match('.*~~>.*', line): rank[12].append(num)


#     # After default
#     elif re.match('.*UESQN\(.*', line): rank[7].append(num)
#     elif re.match('.*splitEqs\(.*', line): rank[6].append(num)
#     elif re.match('.*ARPFEntry\(.*', line): rank[5].append(num)
#     elif re.match('.*!KU\( ~SUPI.*', line): rank[4].append(num)
#     elif re.match('.*!KU\( ~sqn \).*', line): rank[3].append(num)
    
#     # Default
#     else:				   rank[10].append(num)

  

# elif lemma == "injectiveagreement_UE_HSS_AUTN":

# # List of goals in priority order:
#   # (#. < #.
#   # Commit(
#   # KU( ~K )
#   # !KU( f1(
#   # St_2_UE

#   for line in lines:
#     num = line.split(':')[0]
#     if debug:
#       sys.stderr.write(line)

#     # Prio 100
#     if re.match('.*\(\#.+< \#.*', line):
#       rank[100].append(num)

#     # Prio 90
#     elif re.match('.*Commit\(.*', line):
#       rank[90].append(num)

#     # Prio 80
#     elif re.match('.*KU\( ~K \).*', line):
#       rank[80].append(num)

#     # Prio 70
#     elif re.match('.*KU\( f1\(.*', line):
#       rank[70].append(num)

#     # Prio 60
#     elif re.match('.*St_2_UE.*', line):
#       rank[60].append(num)

else:
  if debug:
    sys.stderr.write("No lemma found")
  exit(0)

# Ordering all goals by ranking (higher first)
for listGoals in reversed(rank):
  for goal in listGoals:
    if debug:
      sys.stderr.write(goal)
      print goal

